Herzlich willkommen!

Ja, wir sind weiterhin beim Thema Typinferenz.

Wir haben uns die Definition des Problems gegen Ende der letzten Sitzung angesehen.

Also konkret gegeben ein vorgegebenes Ziel dieser Form hier.

Wir suchen also, naja, gut, das ist hier nur so. Also gegeben einen Kontext, gegeben einen Term und hier eine frische Typvariable.

Wir suchen also eine Typsubstitution Sigma, die uns dieses Problem hier löst.

Und konkreter suchen wir ein allgemeinstes solches Sigma in unserer bekannten Allgemeinheitsordnung auf Substitution.

Und wenn wir das haben, dann ist das hier der Prinzipaltyp unseres vorgegebenen Terms.

Das ist falsch.

So, und wir beschäftigen uns jetzt mit einem tatsächlichen Algorithmus, der uns dieses Typinferenzproblem löst.

Der hat einen angenehmen kurzen Namen, der heißt Algorithmus V, wo auch immer.

Und er stammt von den Herren Hindley und Milner und ist deswegen auch besser bekannt als der Hindley-Milner-Algorithmus.

Und der Hindley-Milner-Algorithmus ist auch tatsächlich der Algorithmus, der hinter den Typinferenzmechanismen von Dingen wie ML oder Haskell eben steckt.

Ja, um den Herren nur recht zu tun, der echte Hindley-Milner-Algorithmus, der kann mehr als nur den einfach getypten Lambda-Kalkül.

Und wir werden den später auch noch auf eine ausdrucksstärkere Sprache erweitern, die dann tatsächlich der Dinge eher Gerechtigkeit tut.

Ja, gut, was ist das Prinzip dieses Algorithmus?

Der Algorithmus, der baut erst mal rekursiv etwas auf und zwar eine Menge von Typgleichungen, die nennen wir PT, zu Ehren des Wortes Prinzipaltyp,

auch wenn das, was da angesammelt wird, zunächst mal noch nicht direkt der Prinzipaltyp ist.

Ja, was kriegt ihr als Argumente? Gut, die kriegt eben drei Argumente, die kriegt eben den Kontext.

Diese Funktion, sie kriegt einen Term und sie kriegt jetzt einen beliebigen Typen, alpha nicht nur eine Typvariable a, sondern irgendeinen Typen.

So, und dann geben wir gleich im Algorithmus noch die Invariante an.

Wir könnten den Algorithmus natürlich direkt angeben und die Invariante hinterher in der Analyse,

aber man versteht den Algorithmus einfach besser, wenn man vorher einmal die Invariante sagt.

Das ist ein allgemeines gutes Prinzip, wer Algorithmen schreibt, sollte immer dazuschreiben, welche Invarianten er da durchdrücken will.

Also, was ist die Eigenschaft, die wir von dieser Menge von Typgleichungen wollen?

Dann nun, wir hatten ja einerseits gesprochen von einem Begriff von Lösung so eines Typisierungsproblems,

also sigma löst das hier, wenn sobald wir sigma hier in gamma und alpha einsetzen, daraus ein hier leitbares Typ urteilt wird.

Und das soll als Invariante genau dann der Fall sein, wenn, genau dann, wenn, so jetzt hatte ich eben erst falsch geschrieben,

wenn sigma ein Unifikator, ja es fehlt eine schließende Klammer hier, wenn sigma ein Unifikator dieser Typmenge, dieser Menge von Typgleichungen hier ist.

Das ist nicht ganz richtig und zwar ist das deswegen nicht ganz richtig, weil diese Menge von Typgleichungen hier mehr Typvariablen enthalten wird, als mein ursprüngliches Typisierungsproblem.

Was wir also komplizierter sagen müssen, ist, dass sigma erweitert zu einem Unifikator von diesem Ding, der also auch die zusätzlichen Variablen substituiert.

Und das drücken wir dadurch aus, dass wir sagen, wenn wir sigma quer einschränken auf die gemeinsamen Typvariablen von gamma und alpha, dass dann genau sigma rauskommt.

So, also in Worten, eine Typsubstitution löst unser Problem genau dann, wenn sie zu einem Unifikator von unserer rekursiv ausgerechneten Menge erweitert wird.

Sagen wir kurz, was wir davon haben, also wir hatten in Algorithmus ein bisschen anders spezifiziert, also beziehungsweise noch gar nicht wirklich spezifiziert.

Also, was haben wir davon? Nun, dann gelten zwei Dinge.

Erstens, unser Typisierungsproblem ist lösbar.

Genau dann, wenn halt unsere Gleichungsmenge unifizierbar ist.

Denn das hier sagt uns gerade jede Lösung hiervon, liefert uns auch eine erweiterte Lösung von unserer Gleichungsmenge.

Und umgekehrt, wenn meine Gleichungsmenge unifizierbar ist, dann kann ich sie einschränken auf die in meinem Typisierungsproblem vorkommenden Typvariablen.

Per Konstruktion ist dieses Ding dann erweiterbar zu einem Unifikator und somit eine Lösung.

Das heißt, wir kriegen also sofort diese Äquivalenz hier.

Und zweitens, etwas salopp formuliert, ja, uns jetzt nichts übertreiben mit der Formalisierung.

Außerdem folgt dann unmittelbar, dass die allgemeinste Lösung unseres Typisierungsproblems nicht der MGU von dem Ding ist,

sondern die Einschränkung des MGU auf die vorkommenden Typvariablen.

Und dann können wir das drittens noch spezialisieren, auf den Fall, dass dieses Alpha nun gerade eine frische Typvariable ist.

Das heißt, wir bekommen irgendein gegebener Term in gegebenem Kontext, der ist typisierbar.

Genau dann, wenn diese Gleichungsmenge jetzt hier mit einer frischen Typvariable unifizierbar ist.

Und in dem Falle, dass wir also Typisierbarkeit haben,

dann ist der Prinzipaltyp von Gamma und T gleich dem MGU, also dem allgemeinsten Unifikator unserer Gleichungsmenge,

das ist dann ja eine Substitution angewendet auf A.